($\lambda$$T$,$x$,$l$,$z$. ($x$ $\in$ $l$)) $\in$ $T$:Type$\rightarrow$$T$$\rightarrow$($T$ List)$\rightarrow\downarrow$True$\rightarrow$Prop